es:ES, i:Id, ds:x:Id fp Type, da:k:Knd fp Type.
es-decls(es;i;ds;da)

{(x:Id. vartype(i;x)  ds(x)?Top)
{& (e:E. loc(e) = i  isrcv(e)  valtype(e)  da(kind(e))?Top)} 

latex

Definitions

P  Q, P  Q, es-decls(es;i;ds;da), {T}, P & Q, vartype(i;x), IdDeq, E, P  Q, P  Q, loc(e), b, isrcv(e), valtype(e), f(x)?z, KindDeq, kind(e), Top, Knd, a:A fp B(a), x:A. B(x), x. t(x), Id, t  T, ES, fpf-domain(f), let x = a in b(x), f(x), Prop, EqDecider(T), (x  l), Unit, x  dom(f), , b, A, xL. P(x), if b t else f fi, xL.P(x), SQType(T), False

Lemmas

Knd sq, bool sq, bool cases, not wf, bnot wf, bool wf, deq wf, subtype rel self, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, member-fpf-domain, fpf-trivial-subtype-top, fpf-domain wf, l member wf, subtype rel wf, fpf-ap wf, let wf, l-all-iff, event system wf, Id wf, fpf wf, Knd wf, top wf, es-kind wf, Kind-deq wf, fpf-cap wf, es-valtype wf, es-isrcv wf, assert wf, es-loc wf, es-E wf, id-deq wf, es-vartype wf, guard wf, es-decls wf